ds:x:Id fp Type, da:k:Knd fp Type, A, B:ecl-trans-tuple{i:l}(ds;da).
ecl-trans-normal(A)
 ecl-trans-normal(B)
 (n:, L':event-info(ds;da) List.
 (ecl-trans-halt2(ds;da;A)(n,L')
 ( (L:event-info(ds;da) List. L'  L  ecl-trans-halt2(ds;da;A)(n,L)))
 (n:, L':event-info(ds;da) List.
 (ecl-trans-halt2(ds;da;B)(n,L')
 ( (L:event-info(ds;da) List. L'  L  ecl-trans-halt2(ds;da;B)(n,L)))
 (n:, L:event-info(ds;da) List. ecl-trans-halt2(ds;da;A)(n,L)  (n  ecl-trans-es(A)))
 (n:, L:event-info(ds;da) List. ecl-trans-halt2(ds;da;B)(n,L)  (n  ecl-trans-es(B)))
 (f:((+Unit)()()), g:(), L:event-info(ds;da) List.
 (x:+Unit.
 (ecl-trans-state(combine-ecl-tuples2(A;B;f;g);L)
 (=
 (<ecl-trans-state(A;L),ecl-trans-state(B;L),x>
 ( ecl-trans-type(combine-ecl-tuples2(A;B;f;g))
 (& (x = inl(true)
 (& (
 (& ((L':event-info(ds;da) List, m:.
 (& ((L'  L
 (& ((& ecl-trans-halt2(ds;da;A)(m,L')
 (& ((& (n:, L'':event-info(ds;da) List.
 (& ((& (L''  L'  ecl-trans-halt2(ds;da;B)(n,L'')  L'' = L')
 (& ((& (n:m. ecl-trans-halt2(ds;da;B)(n,L'))))
 (& (x = inl(false)
 (& (
 (& ((L':event-info(ds;da) List, m:.
 (& ((L'  L
 (& ((& ecl-trans-halt2(ds;da;B)(m,L')
 (& ((& (n:, L'':event-info(ds;da) List.
 (& ((& (L''  L'  ecl-trans-halt2(ds;da;A)(n,L'')  L'' = L')
 (& ((& (n:(m+1). ecl-trans-halt2(ds;da;A)(n,L'))))
 (& (isl(x)  (m:. ecl-trans-halt2(ds;da;A)(m,L) & ecl-trans-halt2(ds;da;B)(m,L)))) 

latex

Definitions

x:A. B(x), ecl-trans-tuple{i:l}(ds;da), P  Q, , x:A. B(x), P & Q, ecl-trans-type(A), combine-ecl-tuples2(A;B;f;g), Prop, t  T, x. t(x), 1of(t), let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), let x = a in b(x), S  T, ecl-trans-state(v;L), ecl-trans-state-from(v;z;L), ecl-trans-init(v), list_accum(x,a.f(x;a);y;l), Y, P  Q, P  Q, False, ecl-trans-halt2(ds;da;A), A, b, isl(x), false, if b t else f fi, ecl-trans-h(v), Top, true, 2of(t), Valtype(da;k), deq-member(eq;x;L), combine-halt-info(ea;eb;f;g;x), reduce(f;k;as), P  Q, {T}, event-info(ds;da), A & B, {i..j}, i  j < k, True, AB, no_repeats(T;l), SQType(T), T, , eqof(d), NatDeq, i=j, (xL.P(x)), xL. P(x), x(s), ecl-trans-normal(x), null(as), Dec(P), , Unit, l1 || l2, (x  l), ecl-trans-es(v),

Lemmas

last induction, ecl-trans-type wf, combine-ecl-tuples2 wf, ecl-trans-state wf, l member wf, decl-state wf, ma-valtype wf, nat wf, bool wf, nat plus wf, subtype rel self, iff wf, btrue wf, iseg wf, ecl-trans-halt2 wf, int seg wf, not wf, le wf, bfalse wf, assert wf, isl wf, event-info wf, unit wf, nat plus inc, ecl-trans-es wf, ecl-trans-normal wf, ecl-trans-tuple wf, fpf wf, Knd wf, Id wf, it wf, iseg nil, decidable false, false wf, ecl-trans-state-append, top wf, ecl-trans-state-from wf, append wf, decidable assert, deq-member wf, Kind-deq wf, iff transitivity, eqtt to assert, assert-deq-member, bnot wf, eqff to assert, assert of bnot, not functionality wrt iff, member append, fpf-cap wf, iseg append, common iseg compat, decidable le, decidable lt, combine-halt-info wf, merge wf, iff functionality wrt iff, priority-select wf, band wf, bor wf, eqof wf, nat-deq wf, l exists wf, priority-select-tt, no repeats cons, no repeats-merge, select wf, length wf1, non neg length, assert of band, and functionality wrt iff, assert of bor, or functionality wrt iff, iseg weakening, squash wf, true wf, iseg append single, decidable int equal, cons member, member-merge, priority-select-ff, l all wf, not-isl-priority-select, priority-select-property, priority-select-inr, ifthenelse wf